Require Import AutoSep.

Definition build_resS := SPEC("d", "s") reserving 0
  PRE[V] [| True |]
  POST[R] [| R = V "d" |].

Definition build := bmodule("build"){{
  bfunction "build_rec"("d", "s", "h")[build_resS]
    If ("s" = 0) {
      Return 0
    } else {
      "h" <-* "s";;
      If ("h" < "d") {
        Return 0
      } else {
        If ("h" = "d") {
          Call "pop"("s");;
          "ret" = Call "Leaf";;
          Return "ret"
        } else {
          "d1" = "d" + 1;;
          "l" = Call "build_rec"("d1", "s");;
          "r" = Call "build_rec"("d1", "s");;
          "ret" = Call "Node"("l", "r");;
          Return "ret"
        }
      }
    };;
    Return "d"
  end  
}}.

Theorem buildOK : moduleOk build.
Proof.
  vcgen.
  post.
  sep auto_ext.
  post.
  evaluate auto_ext.
  sep auto_ext.
  post.
  evaluate auto_ext.
  post.
  evaluate auto_ext.
  sep auto_ext.
Qed.



